D:Dsys.
Feasible(D)
 (v:(i:IdM(i).(timed)state), sched:(Id(?((IdLnk + Id)))),
 (dec:(i,a:IdM(i).state(?if a  dom(M(i).prob) then Outcome else Void fi )), d:(IdId).
 d-comp(D; v; sched; dec; d)
  t:({0..t}(i:Idd-world-state(D;i)))(i:Idd-world-state(D;i))) 

latex

Definitions

t  T, Void, x:AB(x), M.da(a), x:A. B(x), S  T, Dsys, b, finite-type(T), Feasible(M), Feasible(D), s = t, Atom$n, Id, {x:A| B(x)} , , State(ds), M.state, False, A, b, , , P  Q, P & Q, Outcome, if b then t else f fi , locl(a), A  B, , x:A  B(x), P  Q, Unit, left + right, M.dout2(l;tg), M.(timed)state, Type, IdLnk, ma-prob(M;b), b  dom(M.prob), M.din(l,tg), suptype(S; T), d-comp(D; v; sched; dec; d), {i..j}, d-world-state(D;i), M(i), ma-prob-da(M)

Lemmas

dsys wf, d-feasible wf, IdLnk wf, d-comp wf, ma-st wf, ifthenelse wf, ma-prob-dom wf, ma-prob wf, nat wf, unit wf, Id wf, ma-tst wf, d-m wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, p-outcome wf, ma-da wf, locl wf, bnot wf, not wf, assert wf